1. Field of the Invention
The present invention relates to hardware circuit verification; specifically, it relates to verifying whether two different circuits have identical functionality. The present invention particularly relates to a logic verification method that caches knowledge acquired while verifying two subcircuits, and uses this knowledge in future subcircuit comparisons.
2. Background of the Related Art
Recent increases in the complexity of modem integrated circuits have resulted in corresponding increases in the difficulty of verifying design correctness. Design flaws have significant economic impact both in terms of increased time-to-market and in reduced profit margins. A typical design flow has many steps, each of which can introduce design flaws. Traditionally, simulation-based techniques have been used to verify design correctness. These techniques have become less effective because of their inability to completely and quickly verify large designs. An increasingly popular alternative is the use of formal mathematical techniques, employed by tools known as equivalence checkers, to verify design correctness.
A typical design flow where an integrated circuit is taken from concept to fabrication includes a number of steps. As a first step, the conceptual nature of the integrated circuit is determined. The desired functionality of a circuit is described by a set of specifications. A conceptual model of the circuit is created based on the specifications. For example, in the case of a complex microprocessor, the conceptual nature of the circuit is typically specified in a high level language such as C++. Modeling tools are available which simulate the behavior of the conceptual model under specific test cases to ensure.that the model performs as expected.
Once the conceptual nature of the circuit is determined, a register transfer level (RTL) model of the digital circuit is built based upon the conceptual model and is modeled on a digital computer using an RTL modeling tool. At this stage, the design of the circuit, as modeled by the RTL modeling tool, may be used to verify that the circuit meets the desired specifications. In some cases the RTL modeling tool may allow the validity of the modeled circuit to be checked in the context of the high-level language model.
After the design of the RTL model is completed, it is transformed into a gate level model in which individual logic gates are specified and connected together to perform the same logic functions as the RTL level circuit model. The transformation process is error-prone due to both human error and tool error. To validate the transformation, the logic functions of the gate level model must be verified to be the same as the corresponding functions in the RTL model. An equivalence checking tool can be used to perform this verification.
The gate level model is often further transformed by optimizations that attempt to improve the performance of the circuit such as reducing the area required to construct the circuit, increasing the speed of operation of the circuit and reducing the power consumption of the circuit. Once the gate level logic of the circuit model has been optimized, the optimized gate level model operation must be verified with respect to either the RTL level model or the original gate level model.
The gate level model may go though additional transformations, each yielding successive versions of the circuit. An example of this transformation is scan logic insertion, which allows the circuit to perform in a scan mode and a normal mode. When operating in scan mode the circuit can be tested for manufacturing defects, while in normal mode the circuit should behave as before. Another example is clock tree insertion, which is the process of inserting buffers in the clock tree to improve the timing of clock signals.
At some stage the gate level circuit is placed and routed into a layout. This step may involve further transformations and local optimizations that are driven by placement and timing constraints. Each transformation necessitates the verification of functionality of the pre-transformation version compared with the post-transformation version of the circuit.
These stages in the design flow are usually pre-determined and fixed for each specific organization doing circuit design. For example, one particular organization may have the following design stages:                Stage 1: hierarchical RTL design;        Stage 2: hierarchical synthesized design;        Stage 3: hierarchical scan-inserted design;        Stage 4: hierarchical placement-based optimized design;        Stage 5: flat clock-tree inserted design;        Stage 6: final placed and routed flat design.This flow may be different at another design house.        
For each circuit transformation, conventional equivalence checking tools are used to verify the functional equivalence of each pre-transformation version versus the post-transformation version (two designs as successive stages). It is common that the amount of resources (computer time and memory) used to perform this verification is correlated with the degree of difference between the two circuit models being compared. Checking the first RTL circuit model against the final gate-level circuit model is much harder than checking any pair of successive circuit models in the transformation chain. To reduce the resource cost, the conventional methodology is to only compare successive circuit models. However, this introduces a large possibility of errors, because the human user is responsible for managing the various versions, ensuring that no check in the chain was missed, and ensuring that each comparison turns out to be positive. A method for efficiently determining the equivalence between the first RTL circuit model and any derived gate-level version is highly desirable.
In conventional circuit verification, equivalence checking of two circuits is performed by (1) partitioning the two circuits into corresponding combinational subcircuit pairs that contain no storage elements, and (2) combinationally verifying the equivalence of each corresponding subcircuit pair. The circuits are partitioned at circuit inputs, outputs and storage element boundaries. The combinational subcircuit pairs are associated according to a correspondence between the circuit inputs, outputs and storage elements of the two circuits, so that the equivalence is verified for each corresponding set of subcircuits. The conventional device can create the circuit input, output and storage element correspondence with user guidance or automatically—see, e.g., U.S. Pat. No. 5,638,381 to Cho et al. (“the Cho patent”), U.S. Pat. No. 5,949,691 to Kurosaka et al. (“the Kurosaka patent”) and Foster, “Techniques for Higher-Performance Boolean Equivalence Verification”, Hewlett-Packard Journal 30-38 (August 1998).
FIG. 1 shows a conventional system for doing equivalence checking as disclosed by, e.g., the Kurosaka patent. The conventional system reads the circuit data of the two circuits to be compared. It then detects corresponding storage elements in the two circuits. Following this, based on the corresponding storage elements in the two circuits, the circuits are partitioned into many smaller purely combinational portions. The system then has to check each pair of corresponding points and report the results.
More specifically, FIG. 1 describes a conventional system for verifying the equivalence of two circuits. The system reads the circuit data for the two circuits in Step 101. Circuit representation techniques will be readily apparent to those skilled in the art; such techniques may involve converting high-level RTL circuits into an interconnection of gates and registers.
Next, in Step 102 the mapping points, i.e., sequential elements connected to one another by combinational subcircuits, are detected in each of the two circuits by scanning the circuit description. These points include sequential elements such as registers and latches as well as tri-state elements (tri-state elements are not conventionally considered sequential elements; however, they are usually included here in prior art systems because they are easier to handle this way). The mapping points in the two circuits are matched with each other in Step 103 using techniques known in the art—see, e.g., the aforementioned Cho and Kurosawa patents. This mapping and matching reduces the general problem of equivalence checking of sequential circuits to the problem of checking the equivalence of pairs of combinational subcircuits. Typically, no manipulation of the sequential elements is done, so no equivalence checking is implemented for those elements.
The circuits are partitioned into such subcircuits in Step 104 by dividing them at the mapping points. Next, in Step 105 the pairs of combinational subcircuits are checked using conventional methods such as those described in U.S. Pat. No. 5,754,454 to Pixley et al. (“the Pixley patent”). Once the comparison is done, the results are written out or reported to the user in Step 106.
FIG. 2 describes in more detail the conventional method for comparing two combinational subcircuits represented by Step 105 in FIG. 1. This method is similar to those described in C. A. J. van Eijk, “Formal Methods for the Verification of Digital Circuits”, Ph.D. thesis, Eindhoven Institute of Technology, Eindhoven, Netherlands (1997) (“the van Eijk thesis”) or the Pixley patent. First, random simulation (applying randomly-chosen test vectors to the two subcircuits) is run on the two subcircuits in Step 202. Simulation identifies cutpoint pair candidates; i.e., each pair of nets that has the same simulation signature forms a cutpoint pair. The more random simulation vectors chosen, the higher the probability that cutpoint pair candidate passed to the next section actually are cutpoint pairs. These cutpoint pair candidates are assembled into a list for further processing as described below.
If in Step 203 any output pair is determined not to be a cutpoint pair candidate, the system declares nonequivalence based on the simulation signature (two circuits cannot be equivalent if any pair of outputs is not equivalent). Otherwise, in Step 204 a cutpoint pair candidate is selected from the cutpoint pair list. Preferably, this is the candidate closest to the inputs of one or both of the circuits. Although Step 203 might be placed outside the loop bounded by Steps 218 and 216, including it in the loop results in only a minor increase in processor load and allows the routine to jump out of the loop when a pair of subcircuits is discovered to be nonequivalent, rather than running through the whole loop before making the determination.
Using previously gained knowledge of other cutpoints, the combinational equivalence checking engine determines if the pair is equivalent or not in Step 206. Any conventional equivalence checking engine such as the one described in the van Eijk thesis, the Pixley patent or J. R. Burch et al., “Tight Integration of Combinational Verification Methods”, International Conference on Computer-Aided Design (1998) pp. 570-576 (“the Burch paper”), can be used here. Such engines may use many different methods, such as binary decision diagrams (BDDs), automatic test pattern generation (ATPG), satisfiability solvers (SAT), or a combination of these methods.
If at Step 208 the engine determines that the subcircuits are equivalent, it proceeds to see if the cutpoint pair is an output pair in Step 210. If so and Step 212 determines that all outputs have been verified, the job is done and the engine reports equivalence in Step 215. If, on the other hand, Step 210 determines that the candidate is not an output pair or Step 212 determines that all outputs have not been verified, the pair is designated as a real cutpoint pair in Step 214, another potential cutpoint pair is chosen in Step 204, and the cycle is repeated.
On the other hand, if the result of the equivalence check in Step 208 indicates that the pair is not equivalent, and the candidate pair is determined not to be the output pair in Step 216, the subcircuits are determined not to be equivalent (as above, two circuits cannot be equivalent if their outputs are not equivalent) and the test vector which showed the nonequivalence as determined by, e.g., techniques disclosed in the van Eijk thesis or Burch paper is used to refine the cutpoint pair candidates in Step 218 by, e.g., forming groups of subcircuits according to their responses to the simulation vectors.